R:Realizer, es:ES. Consistent(R;es)  Prop 

latex

Definitions

x:A. B(x), t  T, Prop, Consistent(R;es), x. t(x), P & Q, A & B, S  T, S  T, Realizer, Unit, x(s), DeclaredType(ds;x), , , left  right, @loc x initially v:T, @loc only events in L change x:T, only events in L send on lnk with tag, @loc effect knd(v:T)  x := f State(ds) v , sends knd(v:T) on l:tagged(g,State(ds),v):dt, @loc precondition for a(v:T):P State(ds) v, @loc: k writes only members of L, @loc: k sends only on links in L, @loc: only members of L read x

Lemmas

unit wf, Id wf, Knd wf, IdLnk wf, fpf wf, decl-state wf, decl-type wf, true wf, event system wf, init-p wf, frame-p wf, sframe-p wf, effect-p wf, sends-p wf, pre-p wf, aframe-p wf, bframe-p wf, rframe-p wf, es realizer wf